/*
 * VSIDS.cuh
 *
 *  Created on: Dec 4, 2013
 *      Author: jaime
 */

#ifndef VSIDS_CUH_
#define VSIDS_CUH_

#include "../SATSolver/SolverTypes.cuh"
#include <curand_kernel.h>

class VSIDS {
private:
	struct vsids_variable
	{
		int positive_lit_sum;
		int negative_lit_sum;
		bool free;
	};
	const int decay_factor;
	const int clauses_before_decaying;
	const float random_decision_frequency;

	vsids_variable * variables;
	int number_of_variables;

	unsigned long int number_of_decisions;
	unsigned long int number_of_learnt_clauses;

	curandState randState;

	__device__ void initCurand(unsigned long seed);

	__device__ void decay();
	__device__ void increment(Lit literal);
	__device__ Var next_random_var();
	__device__ bool next_random_polarity();
	__device__ Lit next_random_literal();
	__device__ Lit next_higher_literal();

public:
	__device__ VSIDS(int number_of_variables);
	__device__ void free_variable(Var v);
	__device__ void block_variable(Var v);
	__device__ void handle_clause(Clause c);
	__device__ Lit next_literal();

	// Test methods
	__device__ void print();
	__device__ bool is_free(Var v);
};

#endif /* VSIDS_CUH_ */
